1. $T$ : Type
\\[0ex]2. $l_{1}$ : $T$ List
\\[0ex]3. $l_{2}$ : $T$ List
\\[0ex]4. $L$ : $T$ List
\\[0ex]5. $l_{2}$ = ($L$ @ $l_{1}$)
\\[0ex]6. $i$ : $\mathbb{N}$
\\[0ex]7. $i$ $<$ $\parallel$$l_{1}$$\parallel$
\\[0ex]8. $z$ : $T$ List
\\[0ex]9. $z$ = ($L$ @ $l_{1}$)
\\[0ex]$\vdash$  ($l_{1}$[$i$] = $z$[(($\parallel$$z$$\parallel$ {-} $\parallel$$l_{1}$$\parallel$)+$i$)]) $\in$ $\mathbb{P}$